Inference at * 1 1 
Iof proof for Lemma append overlapping sublists:

.....assertion..... NILNIL

1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. i, j:. (i < ||L||)  (j < ||L||)  ((i = j))  ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||}{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9. j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)}{0..||L||}
11. increasing(f;||L2||+1)
12. j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
  ||L1 @ [x / L2]|| = ||L1||+||L2||+1 

latex

 by ((RWO "length_append" 0) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 
C3:n)) (first_tok :t) inil_term))) 

latex

C1: 

C1:   ||L1||+||[x / L2]|| = ||L1||+||L2||+1
C.

Definitions	P & Q, t  T, P  Q, P  Q, P  Q, x:A. B(x)
Lemmas	length wf1, length append